Исчисление Ламбека

Исчисление Ламбека (англ. Lambek calculus, обозначается [math]\displaystyle{ L }[/math]) — формальная логическая система, предложенная в 1958 году Иоахимом Ламбеком, которая предназначена для описания синтаксиса естественных языков. С математической точки зрения исчисление Ламбека является фрагментом линейной логики.

Формальное определение

Исчисление Ламбека можно определить несколькими эквивалентными способами. Ниже представлено определение секвенциального исчисления Ламбека в генценовском виде.

Исчисление Ламбека работает с типами (с точки зрения лингвистики, типы соответствуют определённым категориям слов). Фиксируется множество [math]\displaystyle{ Pr = \{p_1,p_2,\dots\} }[/math], элементы которого называются примитивными типами. Из них строится множество всех типов. Формально, множество [math]\displaystyle{ Tp }[/math] типов исчисления Ламбека — это наименьшее множество, содержащее [math]\displaystyle{ Pr }[/math] и удовлетворяющее следующему свойству: если [math]\displaystyle{ A }[/math], [math]\displaystyle{ B }[/math] — типы, то [math]\displaystyle{ (A\backslash B) }[/math], [math]\displaystyle{ (A\cdot B) }[/math], [math]\displaystyle{ (A/B) }[/math] (скобки часто опускаются) также являются типами. Операции [math]\displaystyle{ \backslash }[/math], [math]\displaystyle{ / }[/math] и [math]\displaystyle{ \cdot }[/math] называются левым делением, правым делением и умножением соответственно.

Примитивные типы принято обозначать строчными латинскими буквами, типы — заглавными латинскими буквами, последовательности типов — заглавными греческими буквами ([math]\displaystyle{ \Gamma }[/math], [math]\displaystyle{ \Delta }[/math] и т. п.).

Секвенцией называется строка вида [math]\displaystyle{ A_1,\dots,A_n\to B }[/math], где [math]\displaystyle{ n \gt 0 }[/math], а [math]\displaystyle{ A_1,\dots,A_n, B }[/math] — типы исчисления Ламбека. Часть слева от стрелки называется антецедентом, а часть после стрелки — сукцедентом.

Аксиомы и правила исчисления Ламбека объясняют, какие секвенции являются выводимыми. Единственная аксиома (точнее, схема аксиом) имеет вид:

[math]\displaystyle{ A\to A }[/math]

В исчислении Ламбека имеется 6 правил вывода, по два на каждую операцию:

[math]\displaystyle{ \cfrac{\Gamma, A,\Delta\to C \quad \Pi\to B}{\Gamma,\Pi, B\backslash A,\Delta\to C}\;(\backslash\to) \qquad \cfrac{B,\Pi\to A}{\Pi\to B\backslash A}\;(\to\backslash) }[/math]

[math]\displaystyle{ \cfrac{\Gamma, A,\Delta\to C \quad \Pi\to B}{\Gamma,A/B,\Pi, \Delta\to C}\;(/\to) \qquad \cfrac{\Pi, B\to A}{\Pi\to A/B}\;(\to/) }[/math]

[math]\displaystyle{ \cfrac{\Gamma, A,B,\Delta\to C}{\Gamma, A\cdot B,\Delta\to C}\;(\cdot\to) \qquad \cfrac{\Gamma\to A\quad \Delta\to B}{\Gamma,\Delta\to A\cdot B}\;(\to\cdot) }[/math]

Секвенция [math]\displaystyle{ \Gamma\to A }[/math] называется выводимой, если её можно получить из аксиом путём применения правил. Соответствующая цепочка аксиом и применений правил называется выводом. Факт выводимости обозначается как [math]\displaystyle{ \mathrm{L}\vdash \Gamma\to A }[/math].

Примеры выводимых секвенций

• Секвенция [math]\displaystyle{ p\to q/(p\backslash q) }[/math] (называемая поднятием типа [math]\displaystyle{ p }[/math]) выводима в исчислении Ламбека:

[math]\displaystyle{ \cfrac{\cfrac{\cfrac{}{q\to q}\quad\cfrac{}{p\to p}}{p,p\backslash q\to q} \quad(\backslash\to)}{p\to q/(p\backslash q)}(\to/) }[/math]

• Секвенция [math]\displaystyle{ p\cdot (q/r)\to (p\cdot q)/r }[/math] выводима в исчислении Ламбека:

[math]\displaystyle{ \cfrac{ \cfrac{ \cfrac{ \cfrac{p\to p \quad q\to q}{p,q\to p\cdot q}(\to\cdot) \quad \cfrac{}{r\to r} } { p, q/r,r\to p\cdot q }(/\to) } { p\cdot (q/r),r\to p\cdot q }(\cdot\to) }{ p\cdot (q/r)\to (p\cdot q)/r }(\to/) }[/math]

• [math]\displaystyle{ \mathrm{L}\vdash p/q,q/r\to p/r }[/math].
• [math]\displaystyle{ \mathrm{L}\vdash (q\backslash p)/r\to q\backslash (p/r) }[/math], [math]\displaystyle{ \mathrm{L}\vdash q\backslash (p/r)\to (q\backslash p)/r }[/math].

Категориальные грамматики Ламбека

Понятие категориальных грамматик Ламбека относится к теории формальных грамматик; они представляют собой частный случай категориальных грамматик. Рассматривается конечное непустое множество [math]\displaystyle{ \Sigma }[/math], называемое алфавитом. [math]\displaystyle{ \Sigma^\ast }[/math] — множество всех строк конечной длины, которые можно составить из символов алфавита [math]\displaystyle{ \Sigma }[/math]; любое подмножество этого множества называется формальным языком.

Категориальная грамматика Ламбека — структура [math]\displaystyle{ \langle \Sigma, S,\triangleright \rangle }[/math] из 3 компонент:

1. [math]\displaystyle{ \Sigma }[/math] — алфавит;
2. [math]\displaystyle{ S\in Tp }[/math] — выделенный тип в грамматике;
3. [math]\displaystyle{ \triangleright\subseteq \Sigma\times Tp }[/math] — конечное бинарное отношение, ставящее в соответствие каждому символу алфавита конечное число типов исчисления Ламбека.

Язык, распознаваемый грамматикой [math]\displaystyle{ \langle \Sigma, S,\triangleright \rangle }[/math], — это множество слов вида [math]\displaystyle{ a_1\dots a_n,\; n\gt 0 }[/math], таких, что для каждого символа [math]\displaystyle{ a_i,\; i=1,\dots,n }[/math] существует соответствующий ему тип [math]\displaystyle{ T_i }[/math] (это означает, что [math]\displaystyle{ a_i\triangleright T_i }[/math]) и [math]\displaystyle{ \mathrm{L}\vdash T_1,\dots,T_n\to S }[/math].

Пример. Пусть [math]\displaystyle{ \Sigma=\{a,b\} }[/math], [math]\displaystyle{ S=s }[/math] — примитивный тип, а отношение [math]\displaystyle{ \triangleright }[/math] задано следующим образом [math]\displaystyle{ a\triangleright s/p }[/math], [math]\displaystyle{ b\triangleright p }[/math], [math]\displaystyle{ b\triangleright s\backslash p }[/math]. Такая грамматика распознает язык [math]\displaystyle{ \{a^nb^n|n\gt 0\} }[/math]. Например, слово [math]\displaystyle{ aaabbb }[/math] принадлежит языку, распознаваемому данной грамматикой, поскольку ему соответствует выводимая секвенция [math]\displaystyle{ s/p,s/p,s/p, p,s\backslash p, s\backslash p\to s }[/math].

Примеры из лингвистики

Если в качестве [math]\displaystyle{ \Sigma }[/math] взять множество слов некоторого естественного языка, появится возможность использовать грамматики Ламбека для описания множества предложений этого языка (или его части). Ставится задача поиска грамматики, которая бы распознавала в точности грамматически верные предложения данного языка или хотя бы корректно описывала некоторые интересующие лингвистов языковые явления. Частные примеры выводимых секвенций, соответствующих грамматически верным предложениям, приведены ниже.

• Английскому предложению John loves Mary "Джон любит Мэри" можно поставить в соответствие секвенцию [math]\displaystyle{ NP, (NP\backslash S)/NP, NP\to S }[/math] . Здесь именам собственным John, Mary соответствует примитивный тип [math]\displaystyle{ NP }[/math] "noun phrase", обозначающий именные группы, а переходному глаголу loves соответствует сложный тип [math]\displaystyle{ (NP\backslash S)/NP }[/math]. Примитивный тип [math]\displaystyle{ S }[/math] "sentence" соответствует повествовательным предложениям. Данная секвенция выводима в исчислении Ламбека:

[math]\displaystyle{ \cfrac{\cfrac{S\to S \quad NP\to NP}{NP, NP\backslash S\to S}(\backslash\to) \quad NP\to NP}{NP, (NP\backslash S)/NP, NP\to S}(/\to) }[/math]

• Более сложному английскому предложению John loves but Bill hates Mary "Джон любит, а Билл ненавидит Мэри" ставится в соответствие выводимая секвенция [math]\displaystyle{ NP, (NP\backslash S)/NP, ((S/NP)\backslash (S/NP))/(S/NP), NP, (NP\backslash S)/NP, NP \to S }[/math] .

Чтобы связать примеры выше с данным в начале раздела формальным определением категориальных грамматик, возьмём в качестве выделенного типа примитивный тип [math]\displaystyle{ S }[/math], а отношение [math]\displaystyle{ \triangleright }[/math] определим так, чтобы словам в английских предложениях выше сопоставлялись соответствующие им в рассмотренных секвенциях типы. Тогда предложения John loves Mary, John loves but Bill hates Mary будут принадлежать языку, распознаваемому данной грамматикой.

Свойства

• В исчислении Ламбека допустимо правило сечения. Иначе говоря, из выводимости секвенций вида [math]\displaystyle{ \Pi\to A }[/math] и [math]\displaystyle{ \Gamma,A,\Delta\to B }[/math] следует выводимость секвенции [math]\displaystyle{ \Gamma,\Pi,\Delta\to B }[/math].
• Класс языков, порождаемых грамматиками Ламбека, совпадает с классом контекстно-свободных языков без пустого слова.
• Задача проверки выводимости секвенции в исчислении Ламбека NP-полна.
• Исчисление Ламбека корректно и полно относительно моделей полугрупп с делением, причём существует универсальная модель. Также оно полно относительно [math]\displaystyle{ L }[/math]-моделей (языковые модели, англ. language models), и относительно [math]\displaystyle{ R }[/math]-моделей (реляционные модели, англ. relational models) .
• В исчисление Ламбека можно добавить аппарат лямбда-исчисления, так что выводы в исчислении Ламбека будут сопровождаться преобразованиями лямбда-типов. С лингвистической точки зрения это позволяет моделировать семантику предложений.

Модификации

Существует ряд вариантов исчисления Ламбека, основанных на добавлении операций, отличных от делений и умножения, и добавлении новых аксиом и правил вывода. Ниже рассмотрены некоторые из вариантов.

• Исчисление Ламбека с единицей ([math]\displaystyle{ L_{\mathbf{1}}^\ast }[/math]). В нём допускаются секвенции вида [math]\displaystyle{ \to B }[/math] (у которых 0 типов в антецеденте). В набор допустимых символов, из которых строятся типы, добавляется единица ([math]\displaystyle{ \mathbf{1} }[/math]). Для неё вводятся одна аксиома и одно правило:

[math]\displaystyle{ \cfrac{}{\to\mathbf{1}} \qquad \cfrac{\Gamma,\Delta\to A}{\Gamma,\mathbf{1},\Delta\to A} }[/math]

• Мультипликативно-аддитивное исчисление Ламбека (multiplicative-additive Lambek calculus) — расширение [math]\displaystyle{ L }[/math], в рамках которого типы строятся не только с помощью делений и умножения, но и с помощью конъюнкции [math]\displaystyle{ \wedge }[/math] и дизъюнкции [math]\displaystyle{ \vee }[/math]. Для них вводятся следующие 6 правил:

[math]\displaystyle{ \cfrac{\Gamma,A_1,\Delta\to C}{\Gamma,A_1\wedge A_2,\Delta\to C}(\wedge_1\to) \qquad \cfrac{\Gamma,A_2,\Delta\to C}{\Gamma,A_1\wedge A_2,\Delta\to C}(\wedge_2\to) }[/math]

[math]\displaystyle{ \cfrac{\Pi\to A_1}{\Pi\to A_1\vee A_2}(\to\vee_1) \qquad \cfrac{\Pi\to A_2}{\Pi\to A_1\vee A_2}(\to\vee_2) }[/math]

[math]\displaystyle{ \cfrac{\Pi\to A_1 \quad \Pi\to A_2}{\Pi\to A_1\wedge A_2}(\to\wedge) \qquad \cfrac{\Gamma,A_1,\Delta\to C \quad \Gamma,A_2,\Delta\to C}{\Gamma,A_1\vee A_2,\Delta\to C}(\vee\to) }[/math]

См. также

• Категориальная грамматика
• Исчисление секвенций

Литература

• Lambek, J. The Mathematics of Sentence Structure (англ.) // The American Mathematical Monthly. — 1958. — Vol. 65, no. 3. — P. 154-170. — ISSN 0002-9890. — doi:10.2307/2310058.
• Moortgat, M. Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus : [англ.]. — Foris Publications. — 1988. — ISBN 9789067653879.
• Пентус М. Р. Исчисление Ламбека и формальные грамматики (рус.) // Фундаментальная и прикладная математика. — 1995. — Т. 1, № 3. — С. 729-751.
• Пентус М. Р. Полнота синтаксического исчисления Ламбека (рус.) // Фундаментальная и прикладная математика. — 1999. — Т. 5, № 1. — С. 193-219.
• Pentus, M. Lambek calculus is NP-complete (англ.) // Theoretical Computer Science. — 2006. — Vol. 357, no. 1. — P. 186-201. — ISSN 0304-3975. — doi:10.1016/j.tcs.2006.03.018.